FDL - Nuprl Lemma : fifo+property

Nuprl Lemma : fifo+property_wf

11,40

es:ES, C, T:Type, S:(C

), R:(C

), codes:(j,i:C

e:{x:E| S(j,i,x)}

state@loc(e)

T),

decodes:(i:C

e:{x:E| R(i,x)}

state@loc(e)

T), Req:(C

), Ack:(C

), i:C,

f:({e:E| R(i,e)}

{e:E|

j:C. (S(j,i,e))} ).
fifo+property(es;codes;decodes;C;S;R;T;Req;Ack;i;f)

Definitions x. t(x), A c B, P Q, P & Q, fifo+property(es;codes;decodes;C;S;R;T;Req;Ack;i;f), t T, x:A. B(x), , x:A. B(x), x(s)

Lemmas event system wf, es-loc wf, es-state wf, causal-order-preserving wf, es-causle wf, es-E wf, antecedent-surjection wf

Definitions	x. t(x), A c B, P Q, P & Q, fifo+property(es;codes;decodes;C;S;R;T;Req;Ack;i;f), t T, x:A. B(x), , x:A. B(x), x(s)
Lemmas	event system wf, es-loc wf, es-state wf, causal-order-preserving wf, es-causle wf, es-E wf, antecedent-surjection wf